Inference at * 1 
Iof proof for Lemma decidable atom equal:



1. a : Atom
2. b : Atom
  (a = b)  ((a = b)) 

latex

 by UseWitness if a=b then inl Ax  else (inr (x.x) ) 

latex

 1: 

 1:   if a=b then inl Ax  else (inr (x.x) )  ((a = b)  ((a = b)))
 .

Definitions

t  T